i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, v:T, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
ds || x : T  R-state-var-init(i;ds;da;x;T;v;ks;tr)  Realizer 

latex

Definitions	x:A. B(x), P  Q, t  T, R-state-var-init(i;ds;da;x;T;v;ks;tr), x. t(x), Prop, x(s)
Lemmas	Rplus wf, R-state-var wf, Rinit wf, fpf-compatible wf, Id wf, id-deq wf, fpf-single wf, Knd wf, l member wf, decl-state wf, ma-valtype wf, fpf wf